\begin{tabbing}
$\forall$$A$, ${\it A'}$:Type.
\\[0ex]strong{-}subtype($A$;${\it A'}$)
\\[0ex]$\Rightarrow$ (\=$\forall$$B$:($A$$\rightarrow$Type), $C$:(${\it A'}$$\rightarrow$Type), ${\it eq}$:EqDecider($A$), ${\it eq'}$:EqDecider(${\it A'}$), $f$, $g$:$a$:$A$ fp$\rightarrow$ $B$($a$).\+
\\[0ex]($\forall$$a$:$A$. $B$($a$) $\subseteq\rho$ $C$($a$)) $\Rightarrow$ \{$f$ $\subseteq$ $g$ $\Rightarrow$ $f$ $\subseteq$ $g$\})
\-
\end{tabbing}